第二章 真偽値の型と数値の型
from 型システムのしくみ
対象言語
trueリテラル
falseリテラル
条件演算子(例: (false ? 1 : 2)、(true ? false : true))
数値リテラル(例: (1)、 (2))
足し算(例: (1 + 2))
判定基準
number型同士以外の足し算はしないこと
条件演算子の条件式がboolean型であること
条件演算子の返す型が一致すること
構文木
https://gyazo.com/7309ae9fb35f564a7c6a9ad8a7296d1c
1 + 2 の構文木
code:ts
{
tag: "add",
left: { tag: "number", n: 1 },
right: {tag: "number", n: 2 },
}
構文木をTypeScriptの型として定義
code:ts
type Term =
| { tag: "true" }
| { tag: "false" }
| { tag: "if"; cond: Term; thn: Term; els: Term }
| { tag: "number"; n: number }
| { tag: "add"; left: Term; right: Term };
tag の代わりに kind や type がよく使われるようだけど、型システムの文脈では kind や type に特別な意味があるので、ここでは tag としている。
項 → Term
本書では、「式」と「文」をまとめて「項」と呼ぶ
パーサー
code:ts
import { parse } from "npm:tiny-ts-parser";
console.log(parse("1 + 2"));
{
tag: "add",
left: {
tag: "number",
n: 1,
loc: { end: { column: 1, line: 1 }, start: { column: 0, line: 1 } }
},
right: {
tag: "number",
n: 2,
loc: { end: { column: 5, line: 1 }, start: { column: 4, line: 1 } }
},
loc: { end: { column: 5, line: 1 }, start: { column: 0, line: 1 } }
}
型の定義
code:ts
type Type =
| { tag: "Boolean" }
| { tag: "Number" };
型検査器の実装
項を受け取ってその項の方を返す関数 typecheck を定義する
code:ts
import { parseArith } from "npm:tiny-ts-parser";
type Term =
| { tag: "true" }
| { tag: "false" }
| { tag: "if"; cond: Term; thn: Term; els: Term }
| { tag: "number"; n: number }
| { tag: "add"; left: Term; right: Term };
;
type Type =
| { tag: "Boolean" }
| { tag: "Number" };
function typecheck(t: Term): Type {
switch (t.tag) {
case "true":
return { tag: "Boolean" }
case "false":
return { tag: "Boolean" }
case "number":
return { tag: "Number" }
case "if":
const condTy = typecheck(t.cond);
if (condTy.tag !== "Boolean") throw "boolean expected";
const thnTy = typecheck(t.thn);
const elsTy = typecheck(t.els);
if (thnTy.tag !== elsTy.tag) {
throw "then and else have different types";
}
return thnTy;
case "add":
const leftTy = typecheck(t.left);
if (leftTy.tag !== "Number") throw "number expected";
const rightTy = typecheck(t.right);
if (rightTy.tag !== "Number") throw "number expected";
return { tag: "Number" }
}
}
console.log(typecheck(parseArith("true")));
console.log(typecheck(parseArith("false")));
console.log(typecheck(parseArith("1")));
console.log(typecheck(parseArith("1 + 2")));
// console.log(typecheck(parseArith("1 + true"))); // number expected
console.log(typecheck(parseArith("true ? 1 : 2")));
// console.log(typecheck(parseArith("1 ? 2 : 3"))); // boolean expected
// console.log(typecheck(parseArith("false ? 1 : false"))); // then and else have different types